(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xb665145d5ed3621e) #x0000b665145d5ed3))
(constraint (= (f #x858e30016e2e9120) #x8ddef3017eeef932))
(constraint (= (f #x7825901eeb22ee47) #x7fa7d91fefb2eee7))
(constraint (= (f #x1d023128dd9ebb06) #x1dd2333adddffbb6))
(constraint (= (f #xc31e39ab30e6ee41) #xcf3ffbbbb3eeeee5))
(constraint (= (f #xede1ee802e597c25) #xeffffee82efdffe7))
(constraint (= (f #x450d1e05ee043851) #x455ddfe5fee47bd5))
(constraint (= (f #x35ed0b35ece55eb8) #x000035ed0b35ece5))
(constraint (= (f #x42d6435d459dd785) #x46ff677dd5dddffd))
(constraint (= (f #x83c8876b0bbd6e29) #x000083c8876b0bbd))
(constraint (= (f #xce20ed0dd275e821) #xcee2efdddf77fea3))
(constraint (= (f #xbc08612e64d4b648) #x0000bc08612e64d4))
(constraint (= (f #x0121250e8124d6a5) #x0133375ee936dfef))
(constraint (= (f #xa0e94bd2b9093dc3) #xaaefdfffbb99bfdf))
(constraint (= (f #x729c4b7082cd839c) #x0000729c4b7082cd))
(constraint (= (f #x1d2e99348be12171) #x1dfef9b7cbff3377))
(constraint (= (f #xb31be048435d70da) #x0000b31be048435d))
(constraint (= (f #x947e14440dacacd2) #x9d7ff5444dfeeedf))
(constraint (= (f #xe3e1d02cd8878b66) #xefffdd2edd8ffbf6))
(constraint (= (f #x44ee9eb753c93350) #x44eeffff77fdb375))
(constraint (= (f #xd889bbed3696131a) #x0000d889bbed3696))
(constraint (= (f #x79553082a8ea8508) #x000079553082a8ea))
(constraint (= (f #xb9d27edba94ba15c) #x0000b9d27edba94b))
(constraint (= (f #xee61512ce6ae4017) #xeee7553eeeeee417))
(constraint (= (f #x6a7ca99b7ace6ae7) #x6effeb9bffeeeeef))
(constraint (= (f #x7683d1162e5344b2) #x77ebfd176ef774fb))
(constraint (= (f #xe6b486ba4483d745) #xeeffcefbe4cbff75))
(constraint (= (f #x9d5c2b8694eb3eea) #x00009d5c2b8694eb))
(constraint (= (f #xca205ee31ee873de) #x0000ca205ee31ee8))
(constraint (= (f #xe6e2e7ee5e7c46ea) #x0000e6e2e7ee5e7c))
(constraint (= (f #xaece17063d0d1dca) #x0000aece17063d0d))
(constraint (= (f #x8370ecc15388e0bd) #x00008370ecc15388))
(constraint (= (f #x7ad7704e5379beee) #x00007ad7704e5379))
(constraint (= (f #xe14216a2097d82da) #x0000e14216a2097d))
(constraint (= (f #x06cb6003454c17c1) #x06eff603755cd7fd))
(constraint (= (f #xe7e48e67953b8221) #xeffecee7fd7bba23))
(constraint (= (f #xb159644aa09ebc1e) #x0000b159644aa09e))
(constraint (= (f #xe7e8edb23e7a05ea) #x0000e7e8edb23e7a))
(constraint (= (f #xe799583c479667aa) #x0000e799583c4796))
(constraint (= (f #xa8ec30669218d156) #xaaeef366fb39dd57))
(constraint (= (f #x2ee12a0ac9ecb534) #x2eef3aaaedfeff77))
(constraint (= (f #x3bec15e3dd99974e) #x00003bec15e3dd99))
(constraint (= (f #xc842dba251cd62c0) #xccc6ffba75ddf6ec))
(constraint (= (f #x53d451cad203e232) #x57fd55deff23fe33))
(constraint (= (f #xb0e3d86747648e99) #x0000b0e3d8674764))
(constraint (= (f #x5287ee8e0cc04bb1) #x57affeeeeccc4fbb))
(constraint (= (f #x33b6465eae1b3228) #x000033b6465eae1b))
(constraint (= (f #xe38bcec1669a8ab7) #xefbbfeed76fbaabf))
(constraint (= (f #xc17591e5778abb1e) #x0000c17591e5778a))
(constraint (= (f #x60cd3127bd1e6147) #x66cdf337ffdfe757))
(constraint (= (f #x17a4d28604412c82) #x17fedfae64453eca))
(constraint (= (f #x261237e1e9293571) #x267337ffffbbb777))
(constraint (= (f #xbe9099e724c3b213) #xbff999ff76cfbb33))
(constraint (= (f #x45b0e990a6b1d0a1) #x45fbef99aefbddab))
(constraint (= (f #x8e8e94657e92b15e) #x00008e8e94657e92))
(constraint (= (f #x07c3d9e457834de8) #x000007c3d9e45783))
(constraint (= (f #x985534ee185de60c) #x0000985534ee185d))
(constraint (= (f #x469e3252060e100a) #x0000469e3252060e))
(constraint (= (f #x9466a4ea0c1aec3b) #x00009466a4ea0c1a))
(constraint (= (f #x0a9eccacded54aee) #x00000a9eccacded5))
(constraint (= (f #x36e5ea3332711c71) #x37effeb333771df7))
(constraint (= (f #x425e5e07cee39364) #x467fffe7feefbb76))
(constraint (= (f #x1a81274c496437c3) #x1ba9377ccdf677ff))
(constraint (= (f #x5da27ab45647c4ad) #x00005da27ab45647))
(constraint (= (f #x2049c2971a0d6e6b) #x00002049c2971a0d))
(constraint (= (f #xcb3936311cc08d5b) #x0000cb3936311cc0))
(constraint (= (f #x349e1e371a7d2684) #x37dffff77bfff6ec))
(constraint (= (f #x11d3425935a74666) #x11df767db7ff7666))
(constraint (= (f #x6a5eedaae1d47a55) #x6effeffaefdd7ff5))
(constraint (= (f #x391e6d0b4e6ec71d) #x0000391e6d0b4e6e))
(constraint (= (f #xaee6de6123791b43) #xaeeeffe7337f9bf7))
(constraint (= (f #x383a80eeecaabc86) #x3bbba8eeeeeabfce))
(constraint (= (f #x9e361592a9e1ecab) #x00009e361592a9e1))
(constraint (= (f #xe6a727d9bdbee6ad) #x0000e6a727d9bdbe))
(constraint (= (f #x8bc8a8ae876c7028) #x00008bc8a8ae876c))
(constraint (= (f #x3eb8e3e88432892b) #x00003eb8e3e88432))
(constraint (= (f #xb966acb06e9dd0d8) #x0000b966acb06e9d))
(constraint (= (f #x6ce825d7b3de87ab) #x00006ce825d7b3de))
(constraint (= (f #x40ad6c160320e731) #x44affed76332ef73))
(constraint (= (f #x15e2ce3da90b418d) #x000015e2ce3da90b))
(constraint (= (f #x3741628b37926bae) #x00003741628b3792))
(constraint (= (f #xe76db6dc5c5c90ce) #x0000e76db6dc5c5c))
(constraint (= (f #x4ea9e94a50cb45d7) #x4eebffdef5cff5df))
(constraint (= (f #xd3b1d5e0649c6432) #xdfbbddfe66dde673))
(constraint (= (f #x2bab93499e6ce021) #x2bbbbb7d9feeee23))
(constraint (= (f #x853e4a7eed709a8b) #x0000853e4a7eed70))
(constraint (= (f #xe6cc145e6d2d988b) #x0000e6cc145e6d2d))
(constraint (= (f #xae69eb0409a9e624) #xaeefffb449bbfe66))
(constraint (= (f #x7178e23ae4d44c40) #x777fee3beedd4cc4))
(constraint (= (f #x1b2d368b55369a8c) #x00001b2d368b5536))
(constraint (= (f #x907163e53202d386) #x997777ff7322ffbe))
(constraint (= (f #x7e1db1e52c83a253) #x7ffdfbff7ecbba77))
(constraint (= (f #x8aad0ece245ba8c8) #x00008aad0ece245b))
(constraint (= (f #x64a47e2932caae4b) #x000064a47e2932ca))
(constraint (= (f #x27545c3bb5871034) #x27755dfbbfdf7137))
(constraint (= (f #xe9029bc9a327ee91) #xef92bbfdbb37fef9))
(constraint (= (f #x8cd0e932331984b3) #x8cddefb333399cfb))
(constraint (= (f #x616bc94baee49e05) #x677ffddfbeeedfe5))
(constraint (= (f #x9e2797569c0c087a) #x00009e2797569c0c))
(constraint (= (f #xcc7bc68a098e02c6) #xccfffeeaa99ee2ee))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000008 x) x) (bvlshr x #x0000000000000010) (bvor (bvudiv x #x0000000000000010) x)))
